ES{i}  Type{i'} 

latex

Definitions	t  T, P  Q, x:A. B(x), loc(e), <a,b>, Id, s = t, x:AB(x), P & Q, EOrderAxioms(E; pred?; info), pred!(e;e'), SWellFounded(R(x;y)), first(e), b, A, Top, Type, f(a), AtomFree(T;x), x:AB(x), IdLnk, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), Unit, left+right, Msg(M), type List, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, kind(e), EqDecider(T), ES
Lemmas	deq wf, EOrderAxioms wf, kind wf, loc wf, Knd wf, kindcase wf, Msg wf, unit wf, val-axiom wf, IdLnk wf, Id wf, atom-free wf, top wf, not wf, assert wf, first wf